Nuprl Definition : insert-by
11,40
postcript
pdf
insert-by(
eq
;
r
;
x
;
l
)
== rec-case(
l
) of [] => [
x
] |
a
::
as
=>
v
.if
eq
(
x
,
a
)
== rec-case(
l
) of [] => [
x
] |
a
::
as
=>
v
.if
then [
a
/
as
]
==
if
r
(
x
,
a
) then [
x
;
a
/
as
] else [
a
/
v
] fi
latex
clarification:
insert-by(
eq
;
r
;
x
;
l
)
== rec-case(
l
) of [] => [
x
/ []] |
a
::
as
=>
v
.if
eq
(
x
,
a
)
== rec-case(
l
) of [] => [
x
/ []] |
a
::
as
=>
v
.if
then [
a
/
as
]
==
if
r
(
x
,
a
) then [
x
;
a
/
as
] else [
a
/
v
] fi
latex
Definitions
rec-case(
a
) of [] =>
s
|
x
::
y
=>
z
.
t
(
x
;
y
;
z
)
,
[]
,
if
b
then
t
else
f
fi
,
f
(
a
)
,
[
car
/
cdr
]
FDL editor aliases
insert-by
origin